Courcelle's theorem

Theorem (Courcelle's theorem)

Let $k \in \mathbb{N}$ and let $\varphi$ be an mso formula over the vocabulary of graphs, i.e. using a binary relation $E(x,y)$. There is a cubic algorithm which inputs a undirected graphs and fails or answers if the graph satisfies $\varphi$. The algorithm succeeeds if the graph has treewidth $\leq k$

References

1. https://www.mimuw.edu.pl/~bojan/20152016-2/jezyki-automaty-i-obliczenia-2/monadic-second-order-logic-and-courcelles-theorem
2. https://en.wikipedia.org/wiki/Courcelle's_theorem
3. https://logic.rwth-aachen.de/files/SeminarMetaWS21/5-Courcelle_Gey.pdf